(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_BV)
(declare-fun v0 () (_ BitVec 5))
(declare-fun v1 () (_ BitVec 6))
(assert (let ((e2(_ bv0 1)))
(let ((e3(_ bv1 1)))
(let ((e4 (concat e3 v0)))
(let ((e5 (concat e2 e2)))
(let ((e6 ((_ sign_extend 1) e3)))
(let ((e7 (ite (= (_ bv1 1) ((_ extract 0 0) v0)) e4 v1)))
(let ((e8 (= e4 ((_ sign_extend 5) e3))))
(let ((e9 (= e3 e2)))
(let ((e10 (= e5 ((_ sign_extend 1) e2))))
(let ((e11 (= e5 ((_ zero_extend 1) e3))))
(let ((e12 (= v1 ((_ zero_extend 5) e3))))
(let ((e13 (= e3 e3)))
(let ((e14 (= e2 e2)))
(let ((e15 (= ((_ zero_extend 5) e3) e7)))
(let ((e16 (distinct ((_ zero_extend 4) e6) e7)))
(let ((e17 (distinct e5 ((_ sign_extend 1) e2))))
(let ((e18 (distinct ((_ sign_extend 5) e3) v1)))
(let ((e19 (distinct e4 e4)))
(let ((e20 (= e3 e3)))
(let ((e21 (distinct ((_ zero_extend 3) e6) v0)))
(let ((e22 (not e21)))
(let ((e23 (xor e13 e20)))
(let ((e24 (xor e22 e16)))
(let ((e25 (and e14 e19)))
(let ((e26 (ite e8 e15 e12)))
(let ((e27 (xor e24 e9)))
(let ((e28 (not e23)))
(let ((e29 (or e25 e28)))
(let ((e30 (or e29 e11)))
(let ((e31 (not e18)))
(let ((e32 (= e30 e17)))
(let ((e33 (or e32 e32)))
(let ((e34 (= e27 e27)))
(let ((e35 (= e26 e31)))
(let ((e36 (and e34 e34)))
(let ((e37 (not e36)))
(let ((e38 (=> e37 e37)))
(let ((e39 (=> e33 e10)))
(let ((e40 (not e35)))
(let ((e41 (and e40 e38)))
(let ((e42 (= e39 e39)))
(let ((e43 (or e41 e41)))
(let ((e44 (=> e42 e43)))
e44
))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
